MASTERARBEIT
Titel der Masterarbeit
On Hilbert’s Tenth Problem over
Rings of Algebraic Integers
Verfasser
Tim Benedikt Herbstrith
angestrebter akademischer Grad
Master of Science (MSc.)
Wien, im Monat Mai 2018
Studienkennzahl lt. Studienblatt: A 033 821
Studienrichtung lt. Studienblatt: Mathematik
Betreuer: ao. Univ.-Prof. Mag. Dr. Ch. Baxa
                    
       
                    
               
         
https://github.com/tim6her/h10-over-rings-of-integers
Vorwort
 

Abstract
 


Contents
1 Prerequisites and central notions 1
    
     
       
     
     
     
      
     
        
  

    
      
2 Hilbert’s tenth problem 55
       
     
    
    
    
               
     
     
A Appendix 99
    
    
  
1 Prerequisites and central notions
            
             
                 
  
               
              
               
               
 
           

1.1 Prerequisites from computability theory
{sec:computability theory}
            
           
            

              
            
                
             
           
              
            
                
          
                
              
               
               
         
1.1.1 Turing machines, problems, and decidability
          01 01

     01    
   
2
1 3
3
1
2
𝑥 = 101
𝑦 = 011
{fig:encoding of graphs}
       
               
         
          

              
           
 
       
              
               
{ex:encoding of graphs}
         
 











             
       

1
          
       
101  011       
              
                
             
                 
                   
          §             
    
§
0 0 0 1
. . .
overflow
{fig:Turing machine}
   
          _      
  
      §_01    
           
start
halt


      
       

 §     §
  §   
 
halt

halt


                
                 
               
                  
   
      §          
             
     
halt
          
 
                   
    0           
 0    
overow
  

overow
0
return
1
             
return
 
 1                  
    
overow
0          
               
 
         
                

   
    
halt
        

start
  §       _    
        
§__
              
                
 
§001_0_
              
01

      


        

§ 


_ 
   
      
 

  
      
 



 
              
             
start
 
           
halt
  
  
         
delta

state

state’



delta "state" b = ("state'", b', m)
             
              
     
delta "state" 1 = ("state'", b', m)
delta "state" b = ("state''", b'', m')
   


state’

 
state
1

state”


state
1
    
{lst:add1}
         
-- start by entering the "overflow" state ...
add1 "start" '§' = ("overflow", '§', 1 )
-- ... and stay in this state, as long as you read only '1'-s
add1 "overflow" '1' = ("overflow", '0', 1 )
-- if you read the first '0' or an empty cell replace it by '1'
-- and enter the "return" state to move the head to the first cell
add1 "overflow" '0' = ("return", '1', -1)
add1 "overflow" '_' = ("return", '1', -1)
-- we finish if we read '§' again or ...
add1 "return" '§' = ("halt", '§', 0 )
-- ... continue to move to the left and don't change the cell
-- content. Here `b` matches '0' or '1'
add1 "return" b = ("return", b , -1)
add1 _state _char = ("error", '_', 0 )
              
              

1
           
{ex:add 1}
     
add1

start
halt
overow
return
error

add1

           
     
                
          
error
   
add1

1101        
    
              
    
     1     0
    01
        
          
  01
         
  
            
      
               
               

1
 https://www.haskell.org/onlinereport/haskell2010
   
§
1 1 0 1
. . .
start
 
start
§
overflow
§
§
1 1 0 1
. . .
overflow
 
overflow
1
overflow
1
§
0 1 0 1
. . .
overflow
 
overflow
1
overflow
1
§
0 0 0 1
. . .
overflow
 
overflow
0
return
1
§
0 0 1 1
. . .
return
 
return
1
return
1
§
0 0 1 1
. . .
return
 
return
1
return
1
§
0 0 1 1
. . .
return
 
return
§
halt
§
§
0 0 1 1
. . .
halt
 
halt
§
halt
§
{fig:complete run}
     
add1
 1101
    
{ex:finite problems are decidable}
               
         
start
halt
accept
reject




           

start




1


1
1 

reject
_ 


0


0
0 

reject
_ 


_

accept
_  


reject
_  

                

    


                  
               
           
        
     _            
    
                
       
        

  

accept
        1   
reject
  
    0  
            
      
accept

reject
     
               
  
                

   
{lem:composition of Turing machines}
  



   


     


  


  

 
start
halt
 
 
     
     

start
§
halt
§ 
    
    

            



  

start
halt


start
halt
   
start
halt
compose
        
  

 
start

compose
 


halt


 
halt

start
 
compose



        
 
     
      
{ex:tally encoding}
   
11
-times
 
    






1 
0
{ex:omega encoding}
         




 
            01
  

    
01
    
    
{lst:tally encoding}
        
-- start by entering the "check" state and ...
tally "start" '§' = ("check", '§', 1 )
-- ... stay in this state while reading only '1'-s
tally "check" '1' = ("check", '1', 1 )
-- on reading '_' accept the input and clear the tape ...
tally "check" '_' = ("accept", '_', -1)
tally "accept" '1' = ("accept", '_', -1)
-- ...except for cell c(1), where you write a '1'
tally "accept" '§' = ("accept", '§', 1 )
tally "accept" '_' = ("halt", '1', -1)
-- however, if you read a '0' first, reject the input
-- by moving to the end of the input string ...
tally "check" '0' = ("rejectMR", '0', 1 )
tally "rejectMR" '_' = ("reject", '_', -1)
tally "rejectMR" b = ("rejectMR", b, 1 ) -- `b` matches '0' or '1'
-- ... and clear the tape except for cell c(1) where you
-- write a '0'
tally "reject" '§' = ("reject", '§', 1 )
tally "reject" '_' = ("halt", '0', -1)
tally "reject" b = ("reject", '_', -1) -- `b` matches '0' or '1'
tally _state _char = ("error", '_', 0 )
                  
        
01
                 
         1         
tally

start
halt
check
accept
reject
rejectMR
error

                 
      1         
 
   
     
 
           
             
          
  
0   
               
              
              

           
   
 

    


     
  



{ex:tally pairing}
             
 

 11
-times
0 11
-times
             
   0      1     

    0    
         
    1      
{ex:total pairing}
       














01

                
               

              01
                 
               
    
        
                    
 §                   
                 
                     
                 
        
            
      




    
   
    
             


             

           
 
 
           


   

    
§
b
1
b
2
. . .
b
n2
b
n1
b
n
. . .
find non-empty
 The machine finds the first non-empty cell.
{fig:total pairing non empty}{sub@fig:total pairing non empty}
§
b
1
b
2
. . .
b
n2
b
n1
b
n
. . .
shift left b
n
 The machine shifts the content of each cell one cell to the left …
{fig:total pairing shift left 1}{sub@fig:total pairing shift left 1}
§
b
1
b
2
b
3
. . .
b
n1
b
n
. . .
shift left b
1
 until it reaches the end of tape symbol §.
{fig:total pairing shift left 2}{sub@fig:total pairing shift left 2}
§
b
1
b
2
b
3
. . .
b
n1
b
n
. . .
find __
 The machine finds two consecutive blank cells and starts over.
{fig:total pairing double blank}{sub@fig:total pairing double blank}{fig:pairing function}
               
               
             
 
   
   
  


 
        
   
  0  

  
{lem:minimization}
  
   
 
 
 
           
             
               
               
     
            
     


   
§ 
__ 
__

   
              
      


     
              
     
§ 
_

_

_

    
         
           
    
             
         
             
           
{pro:characterizations of ce sets}
        
 
      
      
    
 

             
   1           1 
   
   

      1   1  
           

   
  
             
             
         
     

   
§



_
               
                
                 
§

_
         
                 
             

    
{lst:check one}
           1
-- start by entering the "check" state
check1 "start" '§' = ("check", '§', 1 )
-- if you read a 1, check that the next cell is blank, and accept
check1 "check" '1' = ("check_blank", '1', 1 )
check1 "check_blank" '_' = ("accept", '_', -1)
-- if either of these conditions is not the case, reject
check1 "check" b = ("reject", b, 1 )
check1 "check_blank" b = ("reject", b, 1 )
-- accepting and rejecting actions
check1 "accept" 1 = ("halt", 1, -1)
check1 "reject" b = ("error", b, 1)
check1 _state _char = ("error", '_', 0 )
             
        



  

         
          

    
              
           
                  
              



 
   
      
   1          1  
   
             
     
           
                  
             
 
{pro:Posts theorem}
              

             

   
        10 01  
           
             
            
            1
              
          1      
    

    


10100
0
0
0
0
0
            
      1    0    
            
     
      
      

     

    
   
   

     
           
               1     
         
 

       0           
              
  
            
            1       
       
              1     
       
    
          
     
         
     
    1  0        
halt


1.1.2 Church-Turing thesis and the halting problem
               
              
2
            
  
             
  
              
      
2
             

    
{fig:Pinocchio}
                      
 
               
                 
                  
            
            
       

               
                   
               
             
          
        
              
                 
             
             
     
              
   

1   
0     
     
     

   
      0     
       

   
               
        
 
             
        
               
          
 {{eq:m reducibility}}{{eq:m reducibility}}
             
     

   
       
    
     
       
              
              
             
      
{pro:m reducibility and decidability}
    
   
 


      

  

  
        
          

  
           
        
  
  
   
      
       

     

    
               
          
       
  
   


    
              
        
    
 
1.2 Prerequisites from model theory
{sec:model theory}
             
            
               
       
1.2.1 Formulae and models
            
            
            
             
               
             
    
   
                
           
     


   
         
  
   
     
 
 
       

        
     
     
     
    
    


1
e
    
1
 
    e   
      

01
     
   01  
             
             

   
 

      
        
 
   
 
    
 
  
   


   
         
           
              
          
 

        
  


1
e
         

1
e

   
1
   e
      

0  0   
   

  
       
0
1

 
    0
1
        
    

       


      


          

        

               
 

         
  
     
    x
i
 
 
 
   
     
  x
1
x
1
x
2
x
2
1 

     
         
x
2
1
x
2
2
1
 x
2
i
    x
i
x
i
      
        

      
                  
     

       


    
  

       
   x
1
x
n
      x
1
x
n
 
  
  x
1
x
n
  
  x
1
x
n


 
  x
1
x
n
x
i
 

      
  x
1
x
n
   
x
1
x
n

x
1
x
n

x
1
x
n

      
x
1
x
n

x
1
x
n








                 
                
                
 
{lem:terms of rings are polynomials}
          

    
          

  

          
    
     0  1       

  x
i
 

 
   



      

       
    
            

             


1 1 1
-times
       
0 1 1 1
-times
 




   
    
a x
i
1
x
i
d
 a               

   

   
m
1
m
k
 m
i
   
  
        





      

 
     
            
  

     

   
 

3
   

     

               
   
        
 
     
 
               
 
      
 
     


 
  
   

             
 
                

4
               
            
    


 x
1
x
2
x
3
 x
2
x
1
x
2
1
{ex:formula distributivity}
 x
1
x
2
x
3
x
1
x
2
x
3
x
1
x
3
x
2
x
3
3
                
                   
 
4
              x
1
x
1
x
1
     
 

    
       
 x
1
 x
2
 x
3
 x
1
    x
2

       
             
          

     
        x
1
x
2
 x
3
      
     
  x
i
 
     x
i
 
x
i
x
i
         x
i
 
   x
i
         
 x
1
x
2
x
3
  x
2

 x
1
              x
1
x
n

      x
1
x
n
  
            
x
1
x
n
 
 
    
 

       
 
  
 




  

    

 






     
 
  
  
  
 
 




  x
1
x
n
x
1
x
n
 
   
  
               
       
                
 x
2

x
2
x
1
x
2
x
2
x
2
x
3
x
1

                 
                

   
                 
              
x
2
x
1
x
2
x
2
x
4
x
3
x
1

          
              
          
1.2.2 Morphisms, theories, and decidability
{sec:theories}
             
          
              
      
  

      
       
 




    





   

 
 
        

   
      

      
    
 

          
 
       


       

    

         

             
      
   
       
             
                
     
              
      

    
           

   
   
x
1
x
1
e x
1
x
1
e x
1
x
1
x
1
x
2
x
3
x
1
x
2
x
3
x
1
x
2
x
3

x
1
x
1
x
1
1
e
x
1
x
1
1
x
1
e
            
    

  
         




     
             
             

 
  

 

   

       
 
{thm:elementary equivalence}
            
         
      
                
                
     
              
         
          
        
Th

    
        
H10

x
i
1
x
i
k
x
i
1
x
i
k
  

   
          
 
   
  
Th



x
i
1
x
i
k

x
i
1
x
i
k

is atomic, and 
           
              
     

    
x
1
x
1
0x
2
x
1
x
2
1
       Th 
   
      Th
   x
1
x
2
1
1 0        

      Th
   
    Th

     


1
2
4
3
            
          
x
1
x
2
x
3
Ex
1
x
2
Ex
2
x
3
Ex
3
x
1

    x
1
    x
2
x
3
      Th


            
                 
       

    
    

        

        
           


c
         
    
   c
 
             



    
        


 
  
       
H10

x
i
1
x
i
k
x
i
1
x
i
k
  
     
    
        



x
i
1
x
i
k

x
i
1
x
i
k

is atomic, and 
       
    
       


there exists an atomic formula with
, or and 
  
    
    
                 
   
{thm:Diophantine theory}
          


       
      

  P 
       
  

P 

     P  
H10   
    
           


          
    

    
       


     
c
x
i
1
x
i
d
             
      
  P      P    
  
x
i
1
x
i
k
x
i
1
x
i
k


   

     
      
 
 
        

    

 
     
       
 
 
x
i
1
x
i
k
x
i
1
x
i
k
0
 x
i
1
x
i
k
        
  H10            
x
i
1
x
i
k
x
i
1
x
i
k
x
i
1
x
i
k

 

               
 

 





        
  
               
                
            
         
x
                
   
           
 x
j
  
x
-times
    
s


   
x







   

    
              
            
       
               
   


x
1
x
1
0
        
x
0 1
     
       
s 
   






    
            
  

  
              
     
H10
(𝔄)
Th
∃+
(𝔄)
Th(𝔄)
𝐷(𝔄)
H10(𝔄)
𝐷
∃+
(𝔄)
𝐷
𝑐
(𝔄)
                
              
        

           Th

  
 H10
 

    H10
      

   
                
  

            
          
H10
(𝔄)
Th
∃+
(𝔄)
Th(𝔄)
𝐷(𝔄)
H10(𝔄)
𝐷
∃+
(𝔄)
𝐷
𝑐
(𝔄)
𝒦
1.2.3 Computable structures and decidable models
{sec:computable structures}
                
            
               
             
             
              
      
               
         
             
               

            
        
   ar    
                  
            
    
{lem:properties of Goedelization}
            
        
          
  

          
            
       
              
 

    
  x
i
    x
i
        
               
   x
i
 
              
            
             
           
            
             
   FC    R  
F


       
R


       

C
    
            
  
   
         
         


     
  
           
  




       
 

     
    



    
            
  
       

       
 


    

    


    
    
             
             

   
           
  
               
   
    
    
     
      

     
          
     
 
            
            1
           


             
               
 1              
              
11011
   0   1     1
{ex:polynomials are computable}
          

 
 
      

      
  
   
  
     

               
           
{ex:Z is computable}
         

  
         
      

       
           
          
      


    
            
              
    
             
             
             
 
  
     

  

 
 
  

        
                
             
     

          
              
             
          
                
              
{thm:computable categoricity}
          

                 

       
  
        












      


       

  
      
           
     
  
          
             
{ex:N is computably categorical}
         

 
   
 
      
         0

0

  
c

n1
c

n
1

 c
n
       
              
              
     

   
{lem:H10 is semi decidable}
          

 
   H10 
   
         
    
  
  x
1
x
n
x
1
x
n
   

      
   

 



             



  
      H10   
1.3 Prerequisites from number theory
{sec:number theory}
1.3.1 Number fields and rings of algebraic integers
               
               
               
               
         

             
              
        
    
 
 
    

       





   

 
           
              
           
            
             

    
 



         

       


 



      
                
         

             


          
   

    
                 
             
 
            
                 


   

         
               
   
                
             
     
{thm:integral closure}
              
   
          
{pro:characterization of integral elements}
           
            
  
            
            




            
          

   
    
     
 

   
   



      
    
  




      
 

         
           




  
 







  
               
     
{pro:being integral is transitive}
           
    
 
               
 
  
               
              
           
  
   
          
    
     
 
        
               
      
      
    
            
            

    
      
      
    
       
{thm:K is the quotient field of O K}
     
     
        


  

   

      
  
       


   
      
   

  
  

 


    
 
           
   
               


           


     

      






 
        
 
              
  
{thm:primitive element}
            
   
    

 
       

       
    


 
               

            
 
 
     


      



         

   
           

  
     
              
{thm:norm and trace}
              

        

   










 




          
             
  
            
 
 
           
        
              
         
     
  
 
          
       
      
              
              
       

      
           
            







               
  
  

 

     
              
      



  
 
  




  
      
       


  
 

    
  
    



  
          
     
     

 
          
         
  

  

        

            

    

             
               
                  
        
      
       
{cor:O K is computable}
      
     

    


   
          
        
     
       
  
1.3.2 Ideals of
           
           

  
             
     
  



 

      
5
              
           

 








     
         


         
       
    
                 
                
  
               
             
            



5
           

   




                     
            

          

  
  
               
   
            
           

          
{thm:algebraic integers are Dedekind domain}
            
 

     
       
               
         
       
     
                 
           
          

              
   













   





               

    
           
  
            
           
 

             
  

prime ideal

          
6
  
         

prime ideal


prime ideal
       

prime ideal


        
       
 
    
   

              
{thm:Chinese remainder}
     
   
    

      



   





    

           
6
            
    
                  
 

       

   
                
 

 
    






  

     

 

   

 

      

          









   



      




       
 


    
         



    
        
 
          
    


                






      

    
 
   
 

 
               
               
 

    

           

 
   
 



  
   
          

prime ideal

       
           
       



     
        
      
       
        
              
            

  
 
 
1.3.3 Geometry of numbers
               
                
            
          

          



            
   
 
       
   

        


 
      



             

   
𝐷
𝑒
1
𝑒
2
{fig:lattice}
   
   
         
7

  
 


  


  


              
                
    
          
      
                  
     
{thm:Minkowski}
        


            
          


    
        
    

         
 
7
     
           
 

    
 


           

           

 
         
      




             





     
        






       
             


 
      
               
                
       
  
   
  
     
  



  

    
               
      


  
     
{pro:Lagranges four square theorem}
         
     
       

              
     






   




















             
             
          

            


  

       
   
    
             
     
          
  
   
         
        

  
 

          
  
            

    



          
    







 
          


 

   
          

  
        
       
  
             
               
             
     



     

    
                
  
              

             

{thm:Dirichlet}
             
          
             
 


           

        
   



     
    

                

              
       









     





   
          
  









   

   
 








       







     
      





             
 
       
           
                
         
       

   
         
       


   




        
      
               
           
                
               
           
            
                 
       

 
8
      
       
                
       



 


          
  





          

{thm:Dirichlet approximation}
   
          

8
    

    
ႼႵᆡ
ႼႴᆡ ႼႳᆡ
ႼႲᆡ Ⴒᆡ
Ⴓᆡ Ⴔᆡ
Ⴕᆡ
ႼႴᆡ
ႼႳᆡ
ႼႲᆡ
Ⴒᆡ
Ⴓᆡ
Ⴔᆡ
{fig:dirichlet}
          
0
1
;
0 + = 1 +
{fig:unitcircle}
                   
 
      


           
             
              
           
              
           
                 
              
               
    

  
              
                  
         

   
        
          
 


          

                


            
      
    

{{eq:Kronecker 1}}{{eq:Kronecker 1}}
 


              
              

   

        



      
             
         







    
            


      

   
          
       
    
       

  

    
     
       

           

      
 

             

    
       
  
    

    

 
    
    
 
 
{thm:Kronecker}
   
           

      
     

 


             
   

   
               
               
               

     
  
  

  

      
 
       
  
            
 



   

 


          

  {{eq:Kronecker 3}}{{eq:Kronecker 3}}

   

  


{{eq:Kronecker 2}}{{eq:Kronecker 2}}
  




    

       
     

    
 




    
       






   



     
      

     
   

     




 {{eq:Kronecker 4}}{{eq:Kronecker 4}}
              
             
 

 
   

  


   



  
 

       

      


         
1.3.4 Absolute values and local fields
             
              
              
          
     
   

   
  
    
 
      
       
    
            

    
  

  
           
      
 
  
         

    
          





 

         

                
                
              
            
    
       
       
  
            
          


                
            
              
              
             
           
           
   


  
  
 

         

    
              
   

      






         
         
 

  
     
           
{thm:Hasse Minkowski}
       
             
                 
               
             
             
{lem:quadratic form}
         
  
      


  
    
 

       

  
             

          
      
 
 
                
         


      



  
      
{thm:strong approximation}
         
 
       
    


   



          
 
     
       
   
          

2 Hilbert’s tenth problem
2.1 Different perspectives on an old problem
2.1.1 Diophantine equations and sets
              
        
1
   
                
               
   
        
           
              
           
2

       



 

       

                
               
       
3
     
                  
                
      
    
    
  1 
   0 
              
      1  0        
       
               

   1      0 
1
 
2
           
             
                  
   
3
     

  
               
 α  α            
    
         


          
           


  
             

              
       
    
     


  
  







 

       


 

   
      

 






                
 
            
 
   
      
 
          

{ex:Diophantine sets}
              
   



    
          

 
 
     





     

    

 
            

      
  

{ex:being non zero is Diophantine}
     
     
 

          


                

           
   
      
 



              
   



 


         



     


 

    

 
    
     
 

{ex:U K is Diophantine}
               
      

                
               
          
{ex:N is Diophantine over Z}
              
                 
   
          
          

  
    
       
      









  
 

       


  

     

  




    
  

  


            
       

            
              

       


 




                  









         
               




  

       




            
  

    












      









        























         
    

              
           

 
        
 x
1
x
n
y
1
y
m
 

y
1
y
m

y
1
y
m

      
        
     
               
                
               
   H10         
 
     H10
               
     
{lem:intersections and unions}
             
 
   

             
      

            
           
  
   

  
  
 
  


      
 
 
      


 
     
 

            

   

   



            
       


         


  
        



  


  
  
 





   
 
  
 

    



 
 








         
 
 







                  
 

      
             
             
           
              
             
      
  
         
       
           

      
 

             
             
              


        

 


   H10
             
               
         
   
               
 
2.1.2 Purely Diophantine sets
       
     
     


  
  







            
             
               
         

  
           

 
         



x
1
x
n
y
1
y
m
 

y
1
y
m

y
1
y
m

             
               
        
                 
           
  
               
            

              
          
  
          
             
       
             
         
            
                
         
             
               
          
  
 
      

      
 
 



   
            
   
{pro:Diophantine singletons}
             
          
 


    
  

      
           
 
 

         
   

          
            
      



  
      
 




    


     




                
     
    

 
     
 
             
         
       

             
       
      
{thm:purely Diophantine sets}
  
         
             
  
     

  
             
 

       
 





           
   
               
  
  
 
  
     





 

  
     
     
        




          
  
       
 
 

 





              
 
  


      














           

 

    
       
           



                
   
 
   
  





    


 
             

      
        
                 
H10

           
H10
(𝔒
𝐾
)
Th
∃+
(𝔒
𝐾
)
Th(𝔒
𝐾
)
𝐷(𝔒
𝐾
)
H10(𝔒
𝐾
)
𝐷
∃+
(𝔒
𝐾
)
𝐷
𝑐
(𝔒
𝐾
)
𝒦
2.1.3 Related problems
                 
             
             
Th     
4
        
              
          
   
     Th
        
            
            
 
{thmt@@DPRM@data}
{thmt@@DPRM}{thm:DPRM}
           
   
                 
            
{cor:H10 over Z}
        H10    
  
              
          



4
                 
           

  
            
  

          
     
      

    
           
         


   
 


      

y
1
y
m
y
1
y
m
{{eq:representing halting set}}{{eq:representing halting set}}
   H10        
        H10
     H10    
                
                 
               
             
              
                
               
             
                
            

   
              
    
              
 
2.2 Some structural results
             
              
 
{lem:moving up}
  
        
 
 
 

   

 

      
  
    
  

     

 


   
 
    



         
    

 

    
              
                
   
{cor:Diophantine theory is undecidable}
           
           H10 
  
            
             
         
               
         
         

 


  {{eq:halting set is Diophantine}}{{eq:halting set is Diophantine}}
             
     H10
     
         
                 
 
     
       
    
              
   
         
 H10


           

             
           
    
         
           


  
               
 H10

       
                
          
 
{thm:CE sets are Diophantine}
        
      
  
         

  
 
       101
       


-times
  

-times
 
              
      

   

    
 
        












                
    
         
          


















   






















   
       
    
               

                 
          
  
   
          
                 
    

     
             
                  
          
{thm:strong vertical method}
           







   {{eq:sigma x and norm of y}}{{eq:sigma x and norm of y}}





    {{eq:sigma alpha and norm of y}}{{eq:sigma alpha and norm of y}}

 {{eq:x mod alpha}}{{eq:x mod alpha}}

        
               
         
  


  









      












   
       
       
{lem:8}
          
   
   
     





  
 




 
  

  


     









  







 












     





           
       


      
 
  
    




 
               
              
   
    





       
        
      
       
   


   
  



   

     
  










      

 



    
 



     
        





    





    
      
  

  
     





      

 
      
   
  


 
       
 
   
 

               
{lem:approximations of embeddings are Diophantine}
            
  
              
      
    
  
 


  
   
 
     
    
 
  
   

             
  


                
   
        



      


         
2.3 Hilbert’s tenth problem over totally real number fields and
number fields with one pair of non-real embeddings
               
                 
              
                 
                 
            
2.3.1 Finitely many easy lemmas
          
{{eq:Pell}}{{eq:Pell}}

              
               
     
    
 
      
      
  
      
   





 {{eq:def of x and y}}{{eq:def of x and y}}
     
      
    
            

        

 


            

              
 

         
 
 
 
  

 

          
5


 

 
 
   
      
      
       

 
  
           
 
 
         
    

  


          



   



 
          


5
       

  

even

odd

   

even


odd

               
     
        
   
{lem:epsilon is unit}
  
   


{lem:x and y solve Pells equation}

       

   
 
       

  
          
   
 


 





  








     







 
  

         



              

    
           
        



        

 
 
        
    
  
{lem:real part of epsilon}






  
{lem:addition formulas}




        

 


  
 
 

 
  
     

 







 


  



 
      



             

       
     
   
{lem:y m divides y mk}










{lem:x m and y m are relative prime}
    

   
 
              




  
            



 

     









odd


         
   

   

 
  
       


       

        
               


           
          
{lem:recursion for x_m and y_m}
      
    
    







      
   
      




 







         
       
     
    

              
{lem:m congruent y m}

 
{lem:a congruent b mod c}
    

 

 
             
 
       


                
  
       



 
 
          

   
        








 
 

 
{lem:congruence x_2m+k}
      
    
      



            


    









                 
                 
    
       
     
      



          
               

  
  













{lem:forcing divisibility}
       
     
    

             
  
  

     

 

  


 



     
     
 
          

    
 
         
 



{lem:subgroup of ker N L/K}
      
     


    
       



  
  


        



       



   

         
    






  
   









          

              
{lem:rank of N_L/K U_L}
          


  
  


 
    
    


 


 
  
 

      
          
   
 
       


   

    



-times
  

 




     

      


              
     




 {{eq:rank of G}}{{eq:rank of G}}
               
  
           
   
              
               
     


 


 
                
                

  
               
             
           
             
            
           
2.3.2 Diophantine definition of over
               
            
    
        
   
               
       


       
  


    


    
   
      
 
     
        
    
{lem:L over K is quadratic}
         












{{eq:approximations of a}}{{eq:approximations of a}}
 
  
    
  

 
     
    
   

   
             
            
        
     
   

       



 
     
  
        
  




              
         
     


       

 



 




{{eq:def of sigma ij}}{{eq:def of sigma ij}}
  
 
      

   

  
{lem:r and s for tr and opnr}
          
   
 
 




    
 
   
       
    
      
    
     

      




            
 

    








          
  
{lem:properties of sigma epsilon}
          
   
 
        



 


   

{lem:modulus of sigma epsilon}
 


                
          











 
  
    
 
  
   
      

           
       


              
   

  
         
   
    





 


 



        


       

      

  

 
       
             
  
 
       





   
     
  


         
  

     
         
  
      
{lem:approx for delta i 1}
 



{lem:approx for delta i 2}
 

{lem:modulus of elements in the kernel}
 










      




{lem:approximation of epsilon with a}
 

{lem:epsilon is not a root of unity}
    
     

 











    
   



              
       

    














      





  
               
      

    
               
    
    
          


 





 























   

 



  



 
















  



   

          




    
   








  
    








               



by (iv)

        




         

 
    


      
       
          
    
     

          
              

                 

             
 
   
       
     
              
          

   
           
 
         
    
  
       
   

        


    



 






          



 







              
 
  


   


  

     
 
    
 






  


       













 {{eq:approximation of epsilon 0}}{{eq:approximation of epsilon 0}}
 
             









       


























 
      







































{pro:epsilon essentially generaltes G}
       
    
         
               
 
   



    

  
      

    

 






      






 
    












       

      
   
    


    
   
     

    

   

 

         
            

  



     
   



                   
                 
               
     
{cor:forcing sequences}
           

    
    


{{eq:forcing solutions to be sequences}}{{eq:forcing solutions to be sequences}}
   
      



      
             
      
 
 


   

     
       
     
        





              
         

even






odd





          

 

{lem:m smaller x m}
       
    
 



     
       
 

  









    

  
  
{lem:approximations of sigma x and sigma y}
       
    
      
   








           


                  


 



     


  
     
    





        

  


             

   


 
 




  

       
    


 



   





            
   



















{{eq:approximation of sigma x and sigma y}}{{eq:approximation of sigma x and sigma y}}
          
     





 

 
  
   

 


  
  


      


     




      



    


              
  












        
    




    
 


     
    
        
  


 
             
 
  
 
         


  

  

 
 



  
     


  


 
    









 


 
  



     






















 
     






  
  



       
 






   
{lem:defining e}
          
  

         
 
   





{{eq:def of e}}{{eq:def of e}}
        



  






         
     
         



 
   

































             

 
  








        


  









































              
      

      








 {{eq:norm of x eh and x er}}{{eq:norm of x eh and x er}}



       
 


Lem. 2.3.3.(ii)




  








   

 

        




      


  
 
      



     
              









even




odd




  

 

      








  


  

       
{lem:congruences for x m}
          
  





      

  


  
  
   
 
   
   
  









       

  
  
  

   
  






  {{eq:approx of x r1 x r2 and x m}}{{eq:approx of x r1 x r2 and x m}}
   
  

  


        
  



























{{eq:norm of p x}}{{eq:norm of p x}}
             

   
        
















   






























{{eq:norm of x r1 plus x r2}}{{eq:norm of x r1 plus x r2}}
     
 

    






  
         













{{eq:norm of x m and x r1 plus x r2 1}}{{eq:norm of x m and x r1 plus x r2 1}}








{{eq:norm of x m and x r1 plus x r2 2}}{{eq:norm of x m and x r1 plus x r2 2}}
     
   









         







          
  

              
 
 








    
  
































      
    
 
  



        








    
     

      
      


     
    




   
    













         















{lem:def of b}
          
   
 
  
      
  

  
 
  

 
 

 

             
 









  
            


   





   


 
       
        



          











 
             








         
  




      


            
    

  
 












       


      












 
 
 
 
    
   













   
        
  

   
      







  









     
        


 

 
  
             
          
 

              

        
  
   
        
 

           




















 {{eq:sequences}}{{eq:sequences}}






 {{eq:force sequences}}{{eq:force sequences}}


 {{eq:force sequences for w and z}}{{eq:force sequences for w and z}}


 
 {{eq:approx of embeddings 1}}{{eq:approx of embeddings 1}}

 

 
 {{eq:approx of embeddings 2}}{{eq:approx of embeddings 2}}
 {{eq:v is non zero}}{{eq:v is non zero}}
 {{eq:z 2 divides v}}{{eq:z 2 divides v}}
     {{eq:cong 1}}{{eq:cong 1}}
  {{eq:cong 2}}{{eq:cong 2}}
  {{eq:cong 3}}{{eq:cong 3}}





 {{eq:divisibilty of z}}{{eq:divisibilty of z}}
             
           
  
      
              
     
             
             
              

      

         

       

  
  













 






 
          
          
 
             
 

 



 



 


 

        



 


 
 {{eq:approx of embeddings 2 v2}}{{eq:approx of embeddings 2 v2}}
 {{eq:v is non zero v2}}{{eq:v is non zero v2}}

 {{eq:z 2 divides v v2}}{{eq:z 2 divides v v2}}
 

  
 
{{eq:cong 1 v2}}
{{eq:cong 1 v2}}

 
 {{eq:cong 2 v2}}{{eq:cong 2 v2}}
 

 {{eq:cong 3 v2}}{{eq:cong 3 v2}}
       
 
    
 


          
 

 {{eq:j congruent xsi mod y eh}}{{eq:j congruent xsi mod y eh}}
            

 


              
    

 

        
      
   {{eq:k congruent j mod m}}{{eq:k congruent j mod m}}
           

 
          
 


       
 


        







          








               
          

 
         





        

          
 






      
 

      
  
 


 
 

  
      

    


  

   

   

  
             
 



            
 


 
   



 
   
 

       
  
       



           
        
{cor:ZZ is Diophantine over O K}
               
          
       
  
          





             

               
               
                  
              
           
 
            
              
              
        
              
  
        
           
            
  H10
           
            H10
  
                
          

A Appendix
{sec:Appendix}
A.1 Collected Haskell implementations
A.1.1 Simulating Turing machines
{app:turing}
          https://github.com/
tim6her/h10-turing-machines            
 
git clone https://github.com/tim6her/h10-turing-machines.git
cd h10-turing-machines
cabal setup && cabal build && cabal install
             ghci  
              
             
>>> import Automaton.TuringMachine
>>> :l tally
>>> let d = toTransition tally "error" -- mark the errornous state
>>> let turing = TuringMachine "start" '_' "halt" d
>>> "§1111" >>> turing -- Tally encoding of 4
Just "§1"
>>> "§1011" >>> turing -- Not tally encoded
Just "§0"
            
A.1.2 Polynomials
{app:polynomials}
             
             
        
{lst:monomials}
         
{-# LANGUAGE RebindableSyntax #-}
module Monomial
( Monomial
, (<*>)
, idt
, mfromList


, clean
) where
import NumericPrelude
import Data.Map (Map, delete, empty, foldrWithKey, fromList, member, insert,
insertWith, (!))
import Algebra.Monoid as Monoid
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck as QC
-- | Monomials are mappings from ZZ to NN with finite support
newtype Monomial = Monomial (Map Integer Integer) deriving (Eq, Ord)
instance Monoid.C Monomial where
idt = Monomial empty
(<*>) = mmul
instance Show Monomial where
show (Monomial m)
| m == empty = "1"
| otherwise = foldrWithKey
(\x e sh -> "X" ++ show x ++ "^" ++ show e ++ " " ++ sh)
"" m
-- | Creates monomials from list of tuples
--
-- Left entry is index of indeterminate, right index is power of the
-- indeterminate
--
-- === Example
-- >>> mfromList [(1, 2), (0, 3), (4, 7)]
-- X0^3 X1^2 X4^7
mfromList :: [(Integer, Integer)] -> Monomial
mfromList l = clean $ Monomial $ fromList l
-- | Multiplies two monomials
--
-- === Example
-- >>> mmul (mfromList [(1, 2), (2, 4)]) (mfromList [(2, 1), (3, 2)])
-- X1^2 X2^5 X3^2
mmul :: Monomial -> Monomial -> Monomial
mmul xx@(Monomial m1) yy@(Monomial m2)
| m1 == empty = yy

   
| m2 == empty = xx
| otherwise = clean $ Monomial $ foldrWithKey
(\x e m -> if x `member` m
then insertWith (+) x e m
else insert x e m)
m2 m1
clean :: Monomial -> Monomial
clean (Monomial m)
| m == empty = (Monomial m)
| otherwise = Monomial $ foldrWithKey
(\x e m -> if e <= 0
then delete x m
else m)
m m
-- * Testing
main :: IO ()
main = defaultMain tests
tests :: TestTree
tests = testGroup "Tests" [properties, unitTests]
properties :: TestTree
properties = testGroup "Properties" [qcProps]
qcProps = testGroup "Axioms of monoids"
[ QC.testProperty "left multiplication by identity" $
\x -> (let m = mfromList (x :: [(Integer, Integer)])
in idt <*> m == m)
, QC.testProperty "right multiplication by identity" $
\x -> (let m = mfromList (x :: [(Integer, Integer)])
in m <*> idt == m)
, QC.testProperty "associativity" $
\x y z -> (let m1 = mfromList (x :: [(Integer, Integer)])
m2 = mfromList (y :: [(Integer, Integer)])
m3 = mfromList (z :: [(Integer, Integer)])
in (m1 <*> m2) <*> m3 == m1 <*> (m2 <*> m3))
, QC.testProperty "commutativity" $
\x y -> (let m1 = mfromList (x :: [(Integer, Integer)])
m2 = mfromList (y :: [(Integer, Integer)])
in m1 <*> m2 == m2 <*> m1)
]
unitTests = testGroup "Unit tests"


[ testCase "show X0^3 X1^2 X4^7" $
show (mfromList [(1, 2), (0, 3), (4, 7)]) @?= "X0^3 X1^2 X4^7 "
, testCase "sample multiplication" $
show (mmul (mfromList [(1, 2), (2, 4)]) (mfromList [(2, 1), (3, 2)])) @?=
"X1^2 X2^5 X3^2 "
, testCase "test clean" $
mfromList [(1, 0), (2, 0), (3, 1)] @?= mfromList [(3, 1)]
]
{lst:polynomials}
         
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
import NumericPrelude
import qualified Monomial
import qualified Data.Map as Map
import Algebra.Monoid as Monoid
import Algebra.Ring as Ring
import Algebra.Module as Module
import Algebra.Additive as Additive
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck as QC
-- | Polynomials over a ring R are finitely supported functions
-- from the set of monomials to R
newtype Polynomial a = Polynomial (Map.Map Monomial.Monomial a)
-- | Polynomials form an additive (abelian) group
instance (Ring.C a, Eq a) => Additive.C (Polynomial a) where
zero = Polynomial Map.empty
(+) = padd
negate (Polynomial m) = Polynomial $ Map.map negate m
-- | Polynomials from an R-module
instance (Ring.C a, Eq a) => Module.C a (Polynomial a) where
(*>) 0 _ = zero
(*>) a (Polynomial m) = Polynomial $ Map.map (a*) m
-- | Polynomials form a ring with unit
instance (Ring.C a, Eq a) => Ring.C (Polynomial a) where
one = pfromList [(1, [])]
(*) p@(Polynomial m1) q

   
| p == zero = zero
| q == zero = zero
| p == one = q
| q == one = p
| otherwise = Map.foldrWithKey
(\mono coeff poly -> (coeff *> mono `mmul` q) + poly)
0 m1
-- | Two polynomials are equal if their difference is zero
instance (Ring.C a, Eq a) => Eq (Polynomial a) where
(==) p q = let (Polynomial m) = p - q in m == Map.empty
instance (Show a, Eq a) => Show (Polynomial a) where
show (Polynomial p)
| p == Map.empty = "0"
| otherwise = Map.foldrWithKey
(\m a sh -> show a ++ " " ++ show m ++ "+ " ++ sh)
"" p
-- | Adds two polynomials over the same ring
--
-- If a coefficient of a monoid equals 0 the monoid is dropped out of the map
padd :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a -> Polynomial a
padd p@(Polynomial m1) q@(Polynomial m2)
| m1 == Map.empty = q
| m2 == Map.empty = p
| otherwise = clean $ Polynomial $ Map.foldrWithKey
(\mono coeff poly -> if mono `Map.member` poly
then Map.insertWith (+) mono coeff poly
else Map.insert mono coeff poly)
m2 m1
mmul :: (Ring.C a, Eq a) => Monomial.Monomial -> Polynomial a -> Polynomial a
mmul mono poly@(Polynomial mp)
| mono == Monomial.idt = Polynomial mp
| poly == zero = zero
| otherwise = Polynomial $ Map.mapKeys (mono Monomial.<*>) mp
-- | Generate polynomials from lists
pfromList :: (Ring.C a, Eq a) => [(a, [(Integer, Integer)])] -> Polynomial a
pfromList [] = zero
pfromList ((a, m):l) = deepClean . clean $ (Polynomial $ Map.singleton
(Monomial.mfromList m) a) + pfromList l
-- | Comfort function for creating polynomials


--
-- === Example
-- >>> 2 *> ((x 1 + x 2) * (x 1 - x 2)) == 2 *> x 1 ^ 2 - 2 *> x 2 ^ 2
-- True
x :: (Ring.C a, Eq a) => Integer -> Polynomial a
x i = pfromList [(1, [(i, 1)])]
-- | Remove monoids with coefficient zero from support
clean :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a
clean (Polynomial m) = Polynomial $ Map.foldrWithKey
(\mono coeff poly -> if coeff == 0
then Map.delete mono poly
else poly)
m m
-- | Remove variables with power zero from monomials
--
-- This function runs in O(n log(n)) so use it sparsely
deepClean :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a
deepClean (Polynomial m) = Polynomial $ Map.mapKeys Monomial.clean m
-- * Testing
main :: IO ()
main = defaultMain tests
tests :: TestTree
tests = testGroup "Tests" [properties, unitTests]
properties :: TestTree
properties = testGroup "Properties" [qcAddProps, qcModProps,
localOption (QuickCheckTests 5) qcRingProps,
qcAlgebraProps]
qcAddProps = testGroup "Group axioms for addition"
[ QC.testProperty "addition is commutative" $
\x y -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
q = pfromList (y :: [(Int, [(Integer, Integer)])])
in p + q == q + p)
, QC.testProperty "addition is associative" $
\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
p3 = pfromList (z :: [(Int, [(Integer, Integer)])])
in (p1 + p2) + p3 == p1 + (p2 + p3))
, QC.testProperty "addition by zero" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

   
in p + zero == p)
, QC.testProperty "addition with inverse" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in p - p == zero)
]
qcModProps = testGroup "Module axioms"
[ QC.testProperty "first distributive law" $
\a x y -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
q = pfromList (y :: [(Int, [(Integer, Integer)])])
in (a :: Int) *> (p + q) == a *> q + a *> p)
, QC.testProperty "second distributive law" $
\a b x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in (a + b :: Int) *> p == a *> p + b *> p)
, QC.testProperty "multiplications commute" $
\a b x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in (a * b :: Int) *> p == a *> (b *> p))
, QC.testProperty "multiplication by one" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in (one :: Int) *> p == p)
]
qcRingProps = testGroup "Ring axioms"
[ QC.testProperty "multiplication is associative" $
\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
p3 = pfromList (z :: [(Int, [(Integer, Integer)])])
in (p1 * p2) * p3 == p1 * (p2 * p3))
, QC.testProperty "left multiplication by one" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in one * p == p)
, QC.testProperty "right multiplication by one" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in p * one == p)
, QC.testProperty "distributive law" $
\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
p3 = pfromList (z :: [(Int, [(Integer, Integer)])])
in p1 * (p2 + p3) == p1 * p2 + p1 * p3)
]
qcAlgebraProps = testGroup "Algebra axioms"
[ QC.testProperty "multiplications commute" $
\x y a -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
in (a :: Int) *> (p1 * p2) == (a *> p1) * p2)


]
unitTests = testGroup "Unit tests"
[ testCase "sample polynomial" $
show (pfromList [(1, [(1, 2), (3, 4)]), (-4, [(1, 4), (2, 3)])]
:: Polynomial Int) @?= "1 X1^2 X3^4 + -4 X1^4 X2^3 + "
, testCase "test equality" $
pfromList [(0, [(1, 1)])] @?= (zero :: Polynomial Int)
]

Bibliography
         
         
             
       http://www.jstor.org/stable/2269326
             
       10.2307/2371045
        
 
       
         10 . 2307 / 2318447 
http://www.jstor.org/stable/2318447
              
        10. 1016/ j .amc .2005. 09.066 
https://doi.org/10.1016/j.amc.2005.09.066
           
          
            
           
               
      10.2307/1998133
               
      10.2307/2040720
                
           10.1112/jlms/s2-18.3.
385
                
        10.1515/crll.1988.388.189 
https://doi.org/10.1515/crll.1988.388.189
             
      10.1112/jlms/s1-8.1.18
             
      
 


            
            
           
             
10.1007/BF01700692  https://doi.org/10.1007/BF01700692
             
     
             
            
10.1090/S0273-0979-00-00881-8
      
         
    
          
           
        10.1007/978- 3- 642-
75306-0
           
             
          
              
   10.1215/S0012-7094-36-00227-2  https://doi.org/10.
1215/S0012-7094-36-00227-2
           
           
          
  10.1007/978-3-642-54936-6_5
            
       10.1007/978-1-4613-0041-0 
https://doi.org/10.1007/978-1-4613-0041-0
                
  
            
             https://
www.ebook.de/de/product/3665990/david_marker_model_theory_an_introduction.
html
           
       
           www.jmilne.org/
math/


           
    http://www.logic.univie.ac.at/~muellem3/TCS.pdf  

        
    
              
          http : / / ubdata .
univie.ac.at/AC05622932
              
           10.4310/MRL.2013.v20.
n5.a12
              
          10.2307/2047021 
https://doi.org/10.2307/2047021
            
          http://www.ams.org/
notices/200803/tx080300344p.pdf
            
         
           10.1007/3- 540-
45455-1_4
             
            10.1090/S0002-
9904-1944-08111-1  https://doi.org/10.1090/S0002-9904-1944-08111-1
             
          10.2307/2266510
              
        10.2307/2033628  https://doi.
org/10.2307/2033628
            
        10.2307/2266685
              
      10.2307/2269028
               
        10.1515/crll.1986.368.127 
https://doi.org/10.1515/crll.1986.368.127
          
              
  10.1002/cpa.3160420805  https://doi.org/10.1002/cpa.3160420805


           
             10 .
1002/cpa.3160420703
           
            
           https://doi.org/
10.1090/conm/270/04370
           
           
     http : / / www . ebook . de / de / product / 6433593 /
alexandra_shlapentokh _ hilbert_s_tenth_problem_diophantine_classes_and_
extensions_to_global_fields.html
          http://math.
cornell.edu/~shore/papers/pdf/proc4t.pdf   
            
               
        10.1016/S0049-237X(99)
80028-7 http://www.sciencedirect.com/science/article/pii/S0049237X99800287
            
      http://eudml.org/doc/212515
            
             
10.1112/plms/s2-42.1.230  https://doi.org/10.1112/plms/s2-42.1.230

Todo list
   
   
      
        
    
         
    
